p q == if p then tt else q fi  

latex

Up	bool 1, bool 1
Wellformedness Lemmas	bor wf, bor wf
Definitions	if b then t else f fi , tt